Typically a software application is validated through testing where a series of regression tests are run either manually or automatically after each modification of the software. Such testing techniques usually give poor functional coverage of the application under test and, further, may be time consuming. To address these issues, formal verification techniques have emerged as an alternative technology to validate software systems. Such verification tools try to mathematically prove the satisfiability of a specific requirement on a software application or obtain a counterexample in the form of a test case that breaks the requirement—thus, pointing to a bug.
A formal verification system used in software validation typically uses a model checker as its internal proof engine. The checker requires non-deterministic user inputs in the drivers that feed the application being checked. Further, the requirement to be validated is typically specified using a mathematical formalism known as temporal logic, which is difficult for non-formalists to grasp. This has proved to be a significant barrier in the adoption of model checking methods for validating software systems.
The ability to solve verification problems in web applications creates an interesting challenge. As with all such processing operations, of critical importance are issues relating to speed, accuracy, and automation.